Propagate Python assert messages as Laurel property summaries by tautschnig · Pull Request #608 · strata-org/Strata

tautschnig · 2026-03-18T22:50:13Z

Python assert with string message (e.g., assert x > 0, "positive") now flows through as a Laurel property summary. CBMC displays these as property descriptions instead of opaque labels.

Before: [main.1] line 2 assert(38): SUCCESS
After: [main.1] line 2 sum is reflexive: SUCCESS

Only simple string literals are supported; f-strings and non-string messages are silently ignored (the label is used as fallback).

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

Python assert with string message (e.g., assert x > 0, "positive") now flows through as a Laurel property summary. CBMC displays these as property descriptions instead of opaque labels. Before: [main.1] line 2 assert(38): SUCCESS After: [main.1] line 2 sum is reflexive: SUCCESS Only simple string literals are supported; f-strings and non-string messages are silently ignored (the label is used as fallback). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Copilot

Pull request overview

This PR propagates Python assert string-literal messages into Laurel metadata as propertySummary, enabling downstream backends (notably CBMC) to show meaningful property descriptions instead of generated labels.

Changes:

Update Python assert statement translation to capture simple string-literal messages.
Attach the extracted message to the translated Laurel assert via MetaData.withPropertySummary.

Comments suppressed due to low confidence (1)

Strata/Languages/Python/PythonToLaurel.lean:992

This change introduces user-visible behavior (assert message → propertySummary) that is intended to affect downstream reporting (e.g., CBMC property descriptions), but the existing Python golden/e2e tests don’t appear to assert on property summaries. Please add/extend a test that fails if the assert message is not propagated (e.g., inspect generated Laurel/Core metadata or the produced GOTO source-location comment), so regressions are caught automatically.

  | .Assert _ test msg => do
    let condExpr ← translateExpr ctx test
    -- Extract assert message as property summary
    let md := match msg.val with
      | some (.Constant _ (.ConString _ str) _) => md.withPropertySummary str.val
      | _ => md
    -- Check if condition contains a Hole - if so, hoist to variable
    let (condStmts, finalCondExpr, condCtx) :=
      match condExpr.val with
      | .Hole =>
        let freshVar := s!"assert_cond_{test.toAst.ann.start.byteIdx}"
        let varType := mkHighTypeMd .TBool
        let varDecl := mkStmtExprMd (StmtExpr.LocalVariable freshVar varType (some condExpr))
        let varRef := mkStmtExprMd (StmtExpr.Identifier freshVar)
        ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, "bool")] })
      | _ => ([], condExpr, ctx)

    let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert (Any_to_bool finalCondExpr)) md

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Strata/Languages/Python/PythonToLaurel.lean

Shell test verifying the Python→Laurel property summary propagation: creates a Python file with assert messages, translates through the full pipeline (Python → Ion → Laurel → Core → GOTO JSON), and checks that the messages appear as GOTO assert sourceLocation comments. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Shell test verifying the full chain: 1. Laurel assert with summary annotation 2. GOTO JSON contains summary in sourceLocation.comment 3. symtab2gb + CBMC reads the comment 4. CBMC prints the summary as the property description 5. CBMC reports VERIFICATION SUCCESSFUL Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Copilot

Pull request overview

This PR propagates Python assert string messages into Laurel property summaries so that downstream GOTO/CBMC output displays meaningful property descriptions instead of opaque labels.

Changes:

Extend Python→Laurel translation to attach assert ... , "message" as MetaData.propertySummary on generated Laurel assert.
Add a Python-focused regression test that checks the resulting GOTO JSON includes the message in sourceLocation.comment.
Add an end-to-end Laurel→GOTO→CBMC shell test that verifies property summaries appear in CBMC’s output.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 5 comments.

File	Description
Strata/Languages/Python/PythonToLaurel.lean	Extracts constant string assert messages and stores them as property summary metadata.
StrataTest/Languages/Python/tests/test_property_summary.sh	New test that generates GOTO JSON from Python and asserts the summary comment is present.
StrataTest/Backends/CBMC/GOTO/test_property_summary_e2e.sh	New E2E test ensuring property summaries survive through CBMC output.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

StrataTest/Languages/Python/tests/test_property_summary.sh

StrataTest/Backends/CBMC/GOTO/test_property_summary_e2e.sh

Strata/Languages/Python/PythonToLaurel.lean

Address Copilot review feedback: the let md := ... binding shadowed the outer md while also referencing it in the fallback branch. Use md' for the enriched metadata to avoid confusion. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…pefail - test_property_summary.sh: quote \$WORK in trap, use \$PYTHON for verification snippet instead of hardcoded python3 - test_property_summary_e2e.sh: quote \$WORK in trap, enable pipefail so strata failures in pipelines are detected Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Add test_property_summary.sh (Python assert msg → GOTO) and test_property_summary_e2e.sh (Laurel summary → GOTO → CBMC) to the CBMC CI pipeline. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

aqjune-aws

It seems this can potentially help better diagnostics when Core -> SMT path is used too.

keyboardDrummer · 2026-03-19T10:49:56Z

StrataTest/Languages/Python/tests/test_property_summary.sh

@@ -0,0 +1,54 @@
+#!/bin/bash


I have several concerns with a test like this:

It interweaves test framework and test contents code

The test framework part is not reusable.

It mixes programming languages

It's not run on lake test

It's not obvious what the user experience when running Strata on the input program

Can we write this test in Lean so it'll run on lake test ?
Can we place the results that the user will see, inline in the test?

Thank you for pushing me to do the right thing, I admittedly had been cutting a corner here. I believe b1c0e0e implements your request.

Replace the bash/Python test_property_summary.sh with a Lean #eval test that runs on `lake test`. The test compiles a Python file with assert messages through the full pipeline (Python → Ion → Laurel → Core → verify) and checks that the property summaries appear in the VCResults. Uses withPython to skip gracefully when Python is unavailable. The CBMC E2E shell test is kept since it tests external tool integration. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

MikaelMayer · 2026-03-19T13:45:59Z

StrataTest/Backends/CBMC/GOTO/test_property_summary_e2e.sh

+# Verifies that Laurel `assert ... summary "..."` annotations appear in
+# CBMC's verification output as property descriptions.
+
+set -eo pipefail


I feel uncomfortable having a bash script to do this kind of testing. First is this script executed anywhere in the CI? Second, as soon as we want to make more end to end tests, it's likely agents will simply want to make a variation of this file, meaning things will get duplicated and hard to maintain.
At the minimum I would like to see the test program and expectations in two different separate files from the machinery that verifies that the current strata converts the test to the expectations correctly.
That way the machinery can ideally be reused as well.

Yes, this is part of CI. If you are uncomfortable with bash, what would you be comfortable with instead?

keyboardDrummer · 2026-03-20T10:41:59Z

StrataTest/Languages/Python/PropertySummaryTest.lean

+open Strata (pyTranslateLaurel verifyCore)
+
+private meta def testPy : String :=
+"def main(x: int) -> None:


IMO we should use the same style of testing as Laurel uses for Python as well, so this test would simplify to a .lean file containing

def program := # strata program Python; def main(x: int) -> None: assert x == x + 1, "a big lie" # ^^^^^^^^^^ error: a big lie does not hold #end #guard_msgs(drop info, error) in #eval testAnnotatedPython program

I think we should prioritize enabling our Python tests to be written like that.

tautschnig requested a review from a team March 18, 2026 22:50

tautschnig requested review from fabiomadge and keyboardDrummer as code owners March 18, 2026 22:50

Copilot AI review requested due to automatic review settings March 18, 2026 22:50

Copilot AI reviewed Mar 18, 2026

View reviewed changes

Strata/Languages/Python/PythonToLaurel.lean Show resolved Hide resolved

tautschnig and others added 2 commits March 19, 2026 00:19

tautschnig requested a review from Copilot March 18, 2026 23:37

Copilot AI reviewed Mar 18, 2026

View reviewed changes

tautschnig and others added 3 commits March 19, 2026 00:55

Run property summary tests in CBMC CI workflow

a8357d3

Add test_property_summary.sh (Python assert msg → GOTO) and test_property_summary_e2e.sh (Laurel summary → GOTO → CBMC) to the CBMC CI pipeline. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

aqjune-aws added Laurel Python labels Mar 19, 2026

aqjune-aws previously approved these changes Mar 19, 2026

View reviewed changes

Merge branch 'main' into tautschnig/python-assert-messages

f6b1386

tautschnig assigned tautschnig and unassigned tautschnig Mar 19, 2026

keyboardDrummer reviewed Mar 19, 2026

View reviewed changes

tautschnig dismissed aqjune-aws’s stale review via b1c0e0e March 19, 2026 11:57

MikaelMayer reviewed Mar 19, 2026

View reviewed changes

keyboardDrummer reviewed Mar 20, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Propagate Python assert messages as Laurel property summaries#608

Propagate Python assert messages as Laurel property summaries#608
tautschnig wants to merge 8 commits intomainfrom
tautschnig/python-assert-messages

tautschnig commented Mar 18, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

aqjune-aws left a comment

Uh oh!

keyboardDrummer Mar 19, 2026 •

edited

Loading

Uh oh!

tautschnig Mar 19, 2026

Uh oh!

MikaelMayer Mar 19, 2026

Uh oh!

tautschnig Mar 19, 2026

Uh oh!

keyboardDrummer Mar 20, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

tautschnig commented Mar 18, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

aqjune-aws left a comment

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Mar 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig Mar 19, 2026

Choose a reason for hiding this comment

Uh oh!

MikaelMayer Mar 19, 2026

Choose a reason for hiding this comment

Uh oh!

tautschnig Mar 19, 2026

Choose a reason for hiding this comment

Uh oh!

keyboardDrummer Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

keyboardDrummer Mar 19, 2026 •

edited

Loading

keyboardDrummer Mar 20, 2026 •

edited

Loading